…landed (#89)

Updates the `Current rung state (2026-05-20)` block to record Wave 3
of today's swarm and refresh the next-Claude plan.

## What this captures

* 5 Wave-3 PRs (`#80` EchoSearch, `#81` provenance, `#82` absint,
  `#83` parser, `#85` EchoCost) and 2 parallel-session merges
  (`#84` Pillar E Evaluation, `#86` F1 gc-coassoc).
* Axis 8 is now 4-of-4 (decidability + graded access + cost + search).
* Next-Claude plan refreshed: ordinal-track unbudgeted WF is the named
  next bottleneck; EchoApprox examples 6/8 still open; EchoSearch
  sequential/product composition deferred.

## Two minor lessons memorialised

* Per-lane Smoke `open import ... using ( ... )` blocks should be
  separate (with header comments), not shared paren-blocks — cuts
  swarm merge-conflict noise.
* During swarm-merge sequences, re-fetch the branch before any
  force-push: parallel claude sessions may be concurrently rebasing
  the same PR (observed on `#82`).

## Invariants

* Doc-only change; no Agda touched.
* `--safe --without-K` invariant unchanged.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…nstances (#88)

## Summary

Gate **F3** of the earn-back plan (`docs/echo-types/earn-back-plan.adoc
§F3`)
now passes. Two non-isomorphic-grade-monoid instances of an
abstract graded-comonad interface, with no `⊑-prop`-equivalent field
in the interface itself, are mechanised:

* **`nat-instance`** at the **commutative** monoid `(ℕ, +, 0)` —
  packages the F1 (#86) iterated-residue construction.
* **`list-instance`** at the **non-commutative** free monoid
  `(List Tag, ++, [])` over a two-element `Tag` with per-element
  residue layers `R smol A = A × Bool`, `R big A = A × ℕ`. All
  three graded-comonad laws proved.

The non-isomorphism is constructively witnessed by
`tag-list-non-commutative` (one direction: only a non-commutative
monoid satisfies it). The two earn-back gates F1 and F3 — both
landed today — close the comonad-side earn-back programme as
specified.

## Three new modules

### `EchoGradedComonadInterface.agda` — abstract record

`GradedComonadStructure` fields:
* Grade monoid: `G`, `1G`, `_·G_`, the three monoid laws.
* Graded carrier: `D : G → Set → Set`, `mapD`, functor laws.
* Counit `ε : D 1G A → A` at the unit grade.
* **Nested** comultiplication `δ : D (g ·G h) A → D g (D h A)`.
* The three graded-comonad laws stated against `subst` along the
  monoid's propositional identities.

**No `⊑-prop`-equivalent field** — F3 guardrail honoured by
construction. Inspect the field list at the top of the module.

### `EchoGradedComonadInstance1.agda` — F1 packaged

`nat-instance : GradedComonadStructure` reuses
`EchoGradedComonadF1.D / mapD / ε / δ / gc-counit-l / gc-counit-r /
gc-coassoc` verbatim; stdlib's `+-identityˡ / +-identityʳ / +-assoc`
supply the monoid laws. No adapter lemma needed — F1's signatures
already use `subst` along the corresponding ℕ-equation proofs.

### `EchoGradedComonadInstance2.agda` — free-monoid instance

`list-instance : GradedComonadStructure` at `(List Tag, ++, [])`.
Construction parallels F1:
* `D [] A = A`; `D (x ∷ xs) A = R x (D xs A)`.
* `mapD-id`, `mapD-∘` by structural induction (per Tag).
* `D-++` proves the type equality `D (xs ++ ys) A ≡ D xs (D ys A)`
  inductively; `δ = coe (D-++ xs ys A)`.
* `gc-counit-r`: definitional (`++-identityˡ _ = refl` in stdlib).
* `gc-counit-l` / `gc-coassoc`: structural induction on the grade
  list, cons step splitting on the head `Tag`. Same `δ`-naturality
  + `subst`-over-residue factoring as F1's `gc-coassoc`.
* `D-nontrivial`: separating witness that
  `D (smol ∷ big ∷ []) Bool` is not collapsing to `⊤` / a prop.

## Build invariant

* `agda proofs/agda/All.agda` exit 0 under `--safe --without-K`
* `agda proofs/agda/Smoke.agda` exit 0 under `--safe --without-K`
* **zero postulates, no funext, no escape pragmas** anywhere in the
  three new modules
* both instances wired into `All.agda`; record + both instances +
  non-isomorphism witness + non-triviality witness pinned in
  `Smoke.agda`

## Scope (please re-read with care)

F3 earns back the two-models claim **for the graded-comonad witness
introduced by F1** — there are two genuinely non-isomorphic
grade-monoid models of the `GradedComonadStructure` interface, the
laws hold at each, the interface itself is `⊑-prop`-free. That is
exactly what the gate asked for.

F3 does **NOT** earn back the older `EchoRelModel`/`GCLaws`
two-models claim retracted at R-2026-05-18 finding 3. That
retraction concerned `set-model` and `rel-model` (both at the same
grade poset, with `⊑-prop` baked in as a field, `rel-model = set-model
× ⊤`, agreement by `refl`). The `GradedLossModel` interface there
still has `⊑-prop`; that situation is unchanged. F3 here is about a
**different** abstract interface and a **different** pair of models.
The two earn-backs are not interconvertible — do not cite one as
evidence for the other.

`paper.adoc`, `types-abstract.adoc`, and `conservativity.adoc`
remain untouched. Their bodies are about `EchoGraded`'s thin-poset
structure, which neither F1 nor F3 changes. The combined F1+F3
result strengthens the case for a bounded "new contribution"
paragraph, but the title / thesis / reindexing-modality framing
should not move on these gates alone — owner-gated, as for F1.

## Doc updates (gated, scoped)

* `docs/echo-types/earn-back-plan.adoc` — ledger row A3
  (Unstarted → PASSED), Sequencing entry added, Status entry with
  the strict scope qualifier above.
* `docs/retractions.adoc` — follow-up **F-2026-05-20b** appended
  (append-only revision policy preserved); the scope qualifier
  pinned in prose.

## Dependencies

* Builds on **#86** (F1 PASSED). Branch based on
  `f1-coassoc-earn-back`; will rebase cleanly onto `main` once #86
  lands.
* Disjoint from **#82** (AbsInt) and **#84** (paper Evaluation —
  already merged).

## Test plan

* [x] Interface module typechecks
* [x] Instance 1 (nat) typechecks
* [x] Instance 2 (list) typechecks — all three comonad laws
* [x] Full `All.agda` build green
* [x] `Smoke.agda` build green
* [x] No postulates, no escape pragmas, no funext in any new module
* [x] No `⊑-prop`-equivalent field in the interface record
* [x] Non-commutativity witness for the second grade monoid
* [x] Non-triviality witness for the second carrier
* [ ] (owner) inspect field list of `GradedComonadStructure` — flag
      anything `⊑-prop`-shaped if present
* [ ] (owner) ratify the F-2026-05-20b scope language in
      `retractions.adoc`

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

…luster landed

Three small accuracy passes through `docs/echo-types/`:

1. `roadmap.md` §"Theory work — no proof assistant needed" — the
   section is now genuinely closed. Updated two stale items:
   * Axis 8 line said "the *decidability-respecting* candidate has
     shipped" and listed the other three as still candidate
     refinements. All four have now shipped: EchoDecidable
     (decidability), EchoCost (cost-indexed, #85), EchoAccess
     (graded access, #68/#75), EchoSearch (witness-search, #80).
   * Negative / co-echoes line was [unblocked]; now [landed] —
     AntiEcho (#69), tropical decomposition concrete + generic
     (#72 + #91), antiecho-partition-dec (#90). Names the
     obligation-5 / obligation-6 closures explicitly.

2. `roadmap.md` §"Example work" — three [unblocked] items now
   [landed]: ex. 5 (EchoExampleProvenance, #81), ex. 9
   (EchoExampleParser, #83), ex. 10 (EchoExampleAbsInt, #82). Only
   ex. 6 (approximate-echo numeric example) remains [unblocked].

3. `earn-back-plan.adoc`:
   * Header note "the gate discipline was historically attributed
     to a `roadmap-gates.adoc`; that file does not exist in-tree"
     is stale — the file IS in tree (created 2026-05-18). Header
     rewritten to list `roadmap-gates.adoc` alongside
     `retractions.adoc` / this plan / `next-questions.adoc` as the
     four canonical loci.
   * Ledger row D ("roadmap-gates.adoc does not exist") marked
     CLOSED 2026-05-20; cite reflects current reality.

Pure prose / docs only. No Agda content changes. `agda
proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` exit 0
under `--safe --without-K` (verified — confirms the docs say what
the code does).

Refs the closure side of #84 / #86 / #88 / #90 / #91 — does not
modify any Agda module, does not move any earned-back / retracted
claim.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Brings the .machine_readable/6a2/ files in line with the prose docs
following the Pillar F earn-back programme closure and the §"Theory
work" section closing in this session.

META.a2ml — three new ADRs appended (append-only discipline preserved;
no existing ADR edited):

* adr-007 F1 earn-back via monoid-graded iterated-residue construction
  (proofs/agda/EchoGradedComonadF1.agda; PR #86 merged 2026-05-20)
* adr-008 F3 earn-back via two non-isomorphic-grade-monoid instances
  of an abstract interface (EchoGradedComonadInterface +
  Instance1/Instance2; PR #88 open)
* adr-009 Retraction-discipline succeeded: R-2026-05-18 reframing
  converted into four earn-back gate passes (F4, F2, F1, F3); one
  retraction stays retracted (conservativity metatheorem, finding 5);
  none silently re-inflated

Each ADR includes the strict scope qualifier — F1/F3 earn back claims
FOR A SEPARATE SIDE-CONSTRUCTION; EchoGraded itself remains a
thin-poset reindexing modality per R-2026-05-18, and the paper/
types-abstract/conservativity bodies are intentionally not moved.

STATE.a2ml — next-actions list pruned (5 stale April items resolved),
two new sections appended:

* `earn-back-summary` — closure record for all four gates with module
  paths, claim wording, retraction-followup citation, and a
  forbidden-rebrandings list to prevent later mis-framing
* `theory-work-summary` — closure record for §"Theory work — no
  proof assistant needed": axes fully mechanised, ruled-out items,
  refreshed items, canonical examples cluster

next-actions cleaned of long-completed items (the "Apply the
seven-commit integration sequence" entry from April; the t-3 and q2-4
items superseded by intervening work). What remains: q2-1
echo-not-prop generalisation (high), q2-3 RoleGraded as N5 (low),
the new owner-gated-paper-update entry, the in-flight ordinal-track
Path-1 entry (other session), and the parked v0.2 recipe extension.

Pure machine-readable data; no Agda touched. agda proofs/agda/All.agda
and agda proofs/agda/Smoke.agda exit 0 (confirms the schema/format
load with no side-effects on the proof modules).

Refs the closure side of the entire session: #84 / #86 / #88 / #90 /
#91 / #92.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>